////////////////////////////////////////////////////////////////////////////////
// This file is part of the Mist compiler.                                    //
//                                                                            //
// Copyright (C) 2009, 2011 The Mist project                                  //
//                                                                            //
// For a list of contributors, see the COMMITTERS file.                       //
//                                                                            //
// The Mist compiler is free software: you can redistribute it and/or modify  //
// it under the terms of the GNU General Public License as published by       //
// the Free Software Foundation, either version 3 of the License, or          //
// (at your option) any later version.                                        //
//                                                                            //
// The Mist compiler is distributed in the hope that it will be useful,       //
// but WITHOUT ANY WARRANTY; without even the implied warranty of             //
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the              //
// GNU General Public License for more details.                               //
//                                                                            //
// You should have received a copy of the GNU General Public License          //
// in the COPYING file. If not, see <http://www.gnu.org/licenses/>.           //
////////////////////////////////////////////////////////////////////////////////

///
/// \file
/// Contains the definition of all syntax tree node types.
///

#ifndef TREE_HPP
#define TREE_HPP

////////////////////////////////////////////////////////////////////////////////
// Includes                                                                   //
////////////////////////////////////////////////////////////////////////////////

#include <vector>
using std::vector;

#include <set>
using std::set;

#include <map>
using std::map;

#include <boost/optional.hpp>
using boost::optional;

#include <boost/foreach.hpp>
#define foreach BOOST_FOREACH

#include <boost/preprocessor/seq/enum.hpp>
#include <boost/preprocessor/tuple/elem.hpp>
#include <boost/preprocessor/seq/for_each.hpp>
#include <boost/preprocessor/control/if.hpp>
#include <boost/preprocessor/seq/size.hpp>

#include "common/bigint.hpp"
#include "common/computed.hpp"
#include "common/customcomputed.hpp"
#include "accesstype.hpp"
#include "echo.hpp"
#include "keysolver.hpp"
#include "location.hpp"
#include "operator.hpp"
#include "visitor.hpp"

////////////////////////////////////////////////////////////////////////////////
// Forward Declarations                                                       //
////////////////////////////////////////////////////////////////////////////////

CLASSES_FROM( CONCRETE_NODES )

class Symbol;

////////////////////////////////////////////////////////////////////////////////
// Useful Local Macro's                                                       //
////////////////////////////////////////////////////////////////////////////////

#define FROM(name) , public name

#define CLASS(name, base)                            \
	class name : public enable_ptr_this<name> base { \
		public:                                      \
			void accept(wptr<Visitor> v) {           \
				v->visit(wptr_this());               \
			}

#define ROOT_CLASS(name)                           \
	class name {                                   \
		public:                                    \
			virtual ~name() {}                     \
			virtual void accept(wptr<Visitor>) =0;

namespace Detail {
	class Nothing {};
}

#define ABSTRACT_CLASS(name, base)                 \
	class name : virtual Detail::Nothing base {    \
		public:                                    \
			virtual ~name() {}                     \
			virtual void accept(wptr<Visitor>) =0;

#define END_CLASS };

#define CONSTRUCT_PARAM(r, data, param) ( BOOST_PP_TUPLE_ELEM(2, 0, param) BOOST_PP_CAT(_, BOOST_PP_TUPLE_ELEM(2, 1, param) ) )
#define CONSTRUCT_PARAMS(params) BOOST_PP_SEQ_ENUM( BOOST_PP_SEQ_FOR_EACH(CONSTRUCT_PARAM,, params) )
#define CONSTRUCT_INIT(r, data, param) ( BOOST_PP_TUPLE_ELEM(2, 1, param) ( BOOST_PP_CAT(_, BOOST_PP_TUPLE_ELEM(2, 1, param) ) ) )
#define CONSTRUCT_INITS(params) BOOST_PP_SEQ_ENUM( BOOST_PP_SEQ_FOR_EACH(CONSTRUCT_INIT,, params) )
#define CONSTRUCT_VALUE(r, data, param) ( BOOST_PP_CAT(_, BOOST_PP_TUPLE_ELEM(2, 1, param) ) )
#define CONSTRUCT_VALUES(params) BOOST_PP_SEQ_ENUM( BOOST_PP_SEQ_FOR_EACH(CONSTRUCT_VALUE,, params) )
#define BOOST_PP_SEQ_ENUM_0

#define CONSTRUCT(name, params)                                                                              \
	name( CONSTRUCT_PARAMS(params) ) BOOST_PP_IF( BOOST_PP_SEQ_SIZE(params), :, ) CONSTRUCT_INITS(params) {} \
	static sptr<name> construct( CONSTRUCT_PARAMS(params) ) { sptr<name> result(new name( CONSTRUCT_VALUES(params) )); result->scope.set_node(result); return result; }

#define CUSTOM_CONSTRUCT(name, params)                                                                       \
	name( CONSTRUCT_PARAMS(params) ) BOOST_PP_IF( BOOST_PP_SEQ_SIZE(params), :, ) CONSTRUCT_INITS(params) {} \
	static sptr<name> construct( CONSTRUCT_PARAMS(params) ) { sptr<name> result(new name( CONSTRUCT_VALUES(params) )); result->scope.set_node(result);

#define END_CUSTOM_CONSTRUCT return result; }

////////////////////////////////////////////////////////////////////////////////
// Tree Classes                                                               //
////////////////////////////////////////////////////////////////////////////////

/// A node in the abstract syntax tree.
///
ROOT_CLASS( Node )
	/// The optional location of this syntax element in the code.
	///
	optional<Location> location;
	
	/// The scope of this node. It may be set manually, or be determined
	/// automatically when first queried.
	///
	class Scope : public Computed<wptr<Symbol> > {
		void compute_value();
		wptr<Node> _node;
		wptr<Symbol> _manualScope;
		public:
		void set_node(wptr<Node> node);
		wptr<Symbol> operator=(wptr<Symbol> scope);
		void set_automatically(wptr<Symbol> scope);
		bool was_manually_set();
	} scope;
	
	/// The parent of this node. If this is null, this Node
	/// is the root of the AST.
	///
	wptr<Node> parent;
END_CLASS

////////////////////////////////////////////////////////////////////////////////
	
	/// A single identifier / name in the code.
	///
	CLASS( Identifier, FROM(Node) )
		CONSTRUCT( Identifier, ((const string&, text)) )
		
		/// The name of the identifier.
		///
		string text;
		
		/// The optional symbol associated with this identifier if it
		/// was used as a declaration identifier.
		///
		wptr<Symbol> symbol;
	END_CLASS
	
	////////////////////////////////////////////////////////////////////////////
	
	/// A list of declarations in the code.
	///
	CLASS( Declarations, FROM(Node) )
		CONSTRUCT( Declarations, )
		
		/// The declarations.
		///
		vector<sptr<Declaration> > declarations;
	END_CLASS
	
	////////////////////////////////////////////////////////////////////////////
	
	/// A type, such as int, bool or int[].
	///
	ABSTRACT_CLASS( Type, FROM(Node) )
	END_CLASS
	
	////////////////////////////////////////////////////////////////////////////
		
		/// The type of a function.
		///
		CLASS( FunctionType, FROM(Type) )
			CONSTRUCT( FunctionType, )
			CONSTRUCT( FunctionType, ((sptr<Type>, returnType)) )
			CONSTRUCT( FunctionType, ((sptr<Type>, returnType))((const vector<sptr<Type> >&, parameterTypes)) )
			
			/// The return-type of this function.
			///
			sptr<Type> returnType;
			
			/// The parameter-types of this function.
			///
			vector<sptr<Type> > parameterTypes;
		END_CLASS
		
		////////////////////////////////////////////////////////////////////////
		
		/// The type of an array of dynamic size.
		///
		CLASS( ArrayType, FROM(Type) )
			CONSTRUCT( ArrayType, )
			CONSTRUCT( ArrayType, ((sptr<Type>, type)) )
			
			/// The type of the elements of arrays of this this type.
			///
			sptr<Type> type;
		END_CLASS
		
		////////////////////////////////////////////////////////////////////////
		
		/// Primitive or user-defined (Mist >= 0.4) types.
		/// Such as 'int' and '.bool'.
		///
		CLASS( NamedType, FROM(Type) )
			CONSTRUCT( NamedType, )
			CONSTRUCT( NamedType, ((sptr<Reference>, reference)) )
			
			/// The reference to the type. The type-name, possibly with template
			/// parameters.
			///
			sptr<Reference> reference;
		END_CLASS
		
		////////////////////////////////////////////////////////////////////////
		
		/// The void type, which can be returned from functions.
		///
		/// For now, void is a special type. A keyword in the lexer, even.
		/// But in the future (Mist >= 0.3), void will simply be an alias
		/// for the nullary tuple (), and this type of AST node will disappear.
		///
		CLASS( VoidType, FROM(Type) )
			CONSTRUCT( VoidType, )
		END_CLASS
		
		////////////////////////////////////////////////////////////////////////
		
		/// The type of types. Just as '42' is of type 'int',
		/// so is 'int' of type 'type'.
		///
		CLASS( TypeType, FROM(Type) )
			CONSTRUCT( TypeType, )
		END_CLASS
		
	////////////////////////////////////////////////////////////////////////////
	
	/// A statement in the code.
	///
	ABSTRACT_CLASS( Statement, FROM(Node) )
		/// The later computed weakest precondition of this statement for
		/// partial correctness.
		///
		sptr<Expression> partialPrecondition;
		
		/// The later provided postcondition of this statement for
		/// partial correctness.
		///
		sptr<Expression> partialPostcondition;
		
		/// The later computed weakest precondition of this statement for
		/// total correctness.
		///
		sptr<Expression> totalPrecondition;
		
		/// The later provided postcondition of this statement for
		/// total correctness.
		///
		sptr<Expression> totalPostcondition;
	END_CLASS
	
	////////////////////////////////////////////////////////////////////////////
		
		/// A set of assertions.
		///
		CLASS( AssertionArea, FROM(Statement) )
			CONSTRUCT( AssertionArea, )
			CONSTRUCT( AssertionArea, ((const set<sptr<Expression> >&, conditions)) )
			
			/// The assertions that must hold true at that location under any
			/// execution of the code. There is no ordering between subsequent
			/// assertions.
			///
			set<sptr<Expression> > conditions;
		END_CLASS
		
		////////////////////////////////////////////////////////////////////////
		
		/// An 'if' statement that conditionally executes another statement or
		/// statements.
		///
		CLASS( IfStatement, FROM(Statement) )
			CONSTRUCT( IfStatement, )
			CONSTRUCT( IfStatement, ((sptr<Expression>, condition))((sptr<CompoundStatement>, thenStatement)) )
			CONSTRUCT( IfStatement, ((sptr<Expression>, condition))((sptr<CompoundStatement>, thenStatement))((sptr<CompoundStatement>, elseStatement)) )
			
			/// The condition under which the thenStatement is executed.
			///
			sptr<Expression> condition;
			
			/// The statement that is executed if the condition is satisfied.
			///
			sptr<CompoundStatement> thenStatement;
			
			/// The optional statement that is executed if the condition is
			/// not satisfied.
			///
			sptr<CompoundStatement> elseStatement;
		END_CLASS
		
		////////////////////////////////////////////////////////////////////////
		
		/// A 'while' statement that continuously executes its statement while
		/// its condition remains satisfied. Guaranteed to evaluate its
		/// condition at least once. Not guaranteed to ever execute its
		/// statement.
		///
		CLASS( WhileStatement, FROM(Statement) )
			CONSTRUCT( WhileStatement, )

			/// The condition under which the statement continues executing.
			///
			sptr<Expression> condition;

			/// The invariants that must hold:
			/// * each time after evaluation of the while-condition
			/// * each time after execution of the loop body
			///
			set<sptr<AssertionArea> > invariant;

			/// The expression (of type int) that:
			/// * must strictly decrease by each evaluation of the loop body
			/// * must never become smaller than 0
			///
			/// There is room for multiple bounds, but this is
			/// purely for error-reporting purposes. A correct
			/// program has not more than one bound per loop.
			///
			set<sptr<Expression> > bound;

			/// The statement that is executed each time the condition is
			/// tested and satisfied.
			///
			/// There is room for multiple statement sections, but this
			/// is purely for error-reporting purposes. A correct
			/// program has not more than one statement per loop.
			/// (Though it may of course be a compound statement.)
			///
			set<sptr<CompoundStatement> > statement;

			/// The implication: invariant and condition ==> statement.partialPrecondition
			///
			sptr<KeySolver> partialPreImplicationSolver;

			/// The implication: invariant and !condition ==> partialPostcondition
			///
			CustomComputed<sptr<Expression> > partialPostImplication;
			sptr<KeySolver> partialPostImplicationSolver;

			/// The implication: invariant and condition and 0 < bound = oldbound
			///                  ==> statement.totalPrecondition
			///
			CustomComputed<sptr<Expression> > totalPreImplication;
			sptr<KeySolver> totalPreImplicationSolver;

			/// The implication: invariant and !condition ==> totalPostcondition
			///
			CustomComputed<sptr<Expression> > totalPostImplication;
			sptr<KeySolver> totalPostImplicationSolver;
		END_CLASS
		
		////////////////////////////////////////////////////////////////////////
		
		/// A statement that consists of a sequence of smaller statements.
		///
		CLASS( CompoundStatement, FROM(Statement) )
			CUSTOM_CONSTRUCT( CompoundStatement, )
				result->introducedScope.set_node(result);
			END_CUSTOM_CONSTRUCT
			
			CUSTOM_CONSTRUCT( CompoundStatement, ((const vector<sptr<Statement> >&, statements)) )
				result->introducedScope.set_node(result);
			END_CUSTOM_CONSTRUCT
			
			CUSTOM_CONSTRUCT( CompoundStatement, ((sptr<Identifier>, name))((const vector<sptr<Statement> >&, statements)) )
				result->introducedScope.set_node(result);
			END_CUSTOM_CONSTRUCT
			
			/// The optional name of the scope introduced by the
			/// compound statement.
			///
			sptr<Identifier> name;
			
			/// The smaller statements contained in the compound statement.
			///
			vector<sptr<Statement> > statements;
			
			/// The scope that is introduced by this compound-statement.
			///
			Node::Scope introducedScope;
		END_CLASS
		
		////////////////////////////////////////////////////////////////////////
		
		/// A C++ statement. This may only be used by the compiler base file.
		///
		CLASS( CppStatement, FROM(Statement) )
			CONSTRUCT( CppStatement, ((string, code)) )
			
			/// The C++ statement to execute.
			///
			string code;
		END_CLASS
		
		////////////////////////////////////////////////////////////////////////
		
		/// A declaration of a function, variable or type, which can occur
		/// everywhere a statement can occur.
		///
		ABSTRACT_CLASS( Declaration, FROM(Statement) )
		END_CLASS
		
		////////////////////////////////////////////////////////////////////////
			
			/// A declaration of a function.
			///
			CLASS( FunctionDeclaration, FROM(Declaration) )
				CUSTOM_CONSTRUCT( FunctionDeclaration, )
					result->sideEffects.set_function_declaration(result);
					result->paramScope.set_node(result);
					result->resultScope.set_node(result);
				END_CUSTOM_CONSTRUCT
				
				/// The type of the function. This includes the return type
				/// and the types of the parameters.
				///
				sptr<FunctionType> type;
				
				/// The name of the function.
				///
				sptr<Identifier> name;
				
				/// The names of the formal parameters.
				///
				vector<sptr<Identifier> > parameterNames;
				
				/// The names of the formal template parameters.
				///
				vector<sptr<Identifier> > templateTypeNames;
				bool isTemplateInstantiation;
				
				/// The declarations of the logical variables of this
				/// Hoare triple.
				///
				set<sptr<VariableDeclaration> > logicalVars;
				
				/// The preconditions of this Hoare triple.
				///
				set<sptr<AssertionArea> > pre;
				
				/// The postconditions of this Hoare triple.
				///
				set<sptr<AssertionArea> > post;
				
				/// The integer expression that strictly decreases but remains non-negative.
				///
				set<sptr<Expression> > bound;
				
				/// As an alternative to a postcondition, a translation of this
				/// function to a call in KeY, which is used for correctness
				/// proofs.
				///
				/// There is room for multiple KeY translations, but this
				/// is purely for error-reporting purposes. A correct
				/// program has not more than one KeY translation per function.
				///
				set<string> KeY;
				
				/// The implementation of this function in Mist.
				///
				/// There is room for multiple body sections, but this
				/// is purely for error-reporting purposes. A correct
				/// program has not more than one body section per function.
				///
				set<sptr<CompoundStatement> > body;
				
				/// The scope in which the formal parameters live.
				///
				Node::Scope paramScope;
				
				/// The scope in which the result variable lives.
				///
				Node::Scope resultScope;
				
				/// The implication: pre ==> body.weakest_partialPrecondition
				///
				sptr<KeySolver> partialPreImplicationSolver;
				
				/// The implication: pre ==> body.weakest_totalPrecondition
				///
				sptr<KeySolver> totalPreImplicationSolver;
				
				/// A convenient pairing of a formal parameter type and name.
				///
				struct Parameter {
					Parameter(sptr<Type> t, sptr<Identifier> n) : type(t),
					                                              name(n) {}
					sptr<Type>       type;
					sptr<Identifier> name;
				};
				
				/// \return a vector of formal parameters, with both type
				///         and name
				///
				vector<Parameter> parameters() {
					vector<Parameter> result;
					for (unsigned i = 0; i < parameterNames.size(); ++i)
						result.push_back(Parameter(type->parameterTypes[i],
						                           parameterNames[i]));
					return result;
				}
				
				/// The most shallow scope in which this function has
				/// side-effects.
				///
				class SideEffectReach : public Computed<wptr<Symbol> > {
					void compute_value();
					wptr<FunctionDeclaration> _functionDeclaration;
					public: void set_function_declaration(wptr<FunctionDeclaration> functionDeclaration);
				} sideEffects;
			END_CLASS
			
			////////////////////////////////////////////////////////////////////
			
			/// Declaration of a number of variables of the same type.
			///
			CLASS( VariableDeclaration, FROM(Declaration) )
				/// A variable name and initialization together.
				///
				struct Pair {
					Pair() {}
					Pair(sptr<Identifier> n) : name(n) {}
					Pair(sptr<Identifier> n, sptr<Expression> i) : name(n), init(i) {}
					sptr<Identifier> name;
					sptr<Expression> init;
				};
				
				CONSTRUCT( VariableDeclaration, )
				CONSTRUCT( VariableDeclaration, ((sptr<Type>, type))((const vector<Pair>&, pairs)) )
				
				/// The type of the new variables.
				///
				sptr<Type> type;
				
				/// The names and initializations of the new variables.
				///
				vector<Pair> pairs;
			END_CLASS
			
			////////////////////////////////////////////////////////////////////
			
			/// A declaration of a type in Mist. It specifies translations
			/// to C++ and to KeY.
			///
			/// In the future, type declarations can also be used to alias
			/// existing (composed) types.
			///
			CLASS( TypeDeclaration, FROM(Declaration) )
				CONSTRUCT( TypeDeclaration, )
				CONSTRUCT( TypeDeclaration, ((sptr<Identifier>, name))((string, cpp))((string, KeY)) )
				
				/// The name of the type in Mist.
				///
				sptr<Identifier> name;
				
				/// Translation of this type to C++.
				///
				string cpp;
				
				/// Translation of this type to KeY.
				///
				string KeY;
			END_CLASS
			
		////////////////////////////////////////////////////////////////////////
		
		/// An expression in Mist.
		///
		ABSTRACT_CLASS( Expression, FROM(Statement) )
			/// The type of the expression.
			///
			class TypeOf : public Computed<sptr<Type> > {
				void compute_value();
				wptr<Expression> _expression;
				public: void set_expression(wptr<Expression> expression);
			} type;
			
			/// The access-type of the expression. This is computed in a later
			/// compiler phase.
			///
			class AccessTypeOf : public Computed<AccessType> {
				void compute_value();
				wptr<Expression> _expression;
				public: void set_expression(wptr<Expression> expression);
			} access;
			
			/// The shallowest scope that the side-effects of this expression reach.
			/// Valued null if this expression has no side effects. This is
			/// computed in a later compiler phase.
			///
			class SideEffectReach : public Computed<wptr<Symbol> > {
				void compute_value();
				wptr<Expression> _expression;
				public: void set_expression(wptr<Expression> expression);
			} sideEffects;
		END_CLASS
		
		////////////////////////////////////////////////////////////////////////
			
			/// A function-call, which can take parameters, can return a value
			/// and potentially introduces side-effects.
			///
			CLASS( FunctionCall, FROM(Expression) )
				CUSTOM_CONSTRUCT( FunctionCall, )
					result->type.set_expression(result);
					result->access.set_expression(result);
					result->sideEffects.set_expression(result);
				END_CUSTOM_CONSTRUCT
				
				CUSTOM_CONSTRUCT( FunctionCall, ((sptr<Expression>, base))((vector<sptr<Expression> >, parameters)) )
					result->type.set_expression(result);
					result->access.set_expression(result);
					result->sideEffects.set_expression(result);
				END_CUSTOM_CONSTRUCT
				
				/// The base of the function-call. In the current Mist language,
				/// this may only be a reference to a function. But in the future,
				/// this may be any expression of a function type.
				///
				sptr<Expression> base;
				
				/// The actual parameters of the function call.
				///
				vector<sptr<Expression> > parameters;
			END_CLASS
			
			////////////////////////////////////////////////////////////////////
			
			/// An operation using an operator symbol. Takes one or two parameters,
			/// and potentially introduces side-effects.
			///
			CLASS( OperatorCall, FROM(Expression) )
				CUSTOM_CONSTRUCT( OperatorCall, )
					result->type.set_expression(result);
					result->access.set_expression(result);
					result->sideEffects.set_expression(result);
				END_CUSTOM_CONSTRUCT
				
				CUSTOM_CONSTRUCT( OperatorCall, ((sptr<Operator>, op)) )
					result->type.set_expression(result);
					result->access.set_expression(result);
					result->sideEffects.set_expression(result);
				END_CUSTOM_CONSTRUCT
				
				/// The operator of this operation.
				///
				sptr<Operator> op;
				
				/// The operands of this operation.
				///
				vector<sptr<Expression> > operands;
			END_CLASS
			
			////////////////////////////////////////////////////////////////////
			
			/// A reference to a symbol in the program; to a function, variable,
			/// type or named scope.
			///
			CLASS( Reference, FROM(Expression) )
				CUSTOM_CONSTRUCT( Reference, )
					result->type.set_expression(result);
					result->symbol.set_reference(result);
					result->access.set_expression(result);
					result->sideEffects.set_expression(result);
				END_CUSTOM_CONSTRUCT
				
				CUSTOM_CONSTRUCT( Reference, ((string, namePart)) )
					result->type.set_expression(result);
					result->symbol.set_reference(result);
					result->access.set_expression(result);
					result->sideEffects.set_expression(result);
				END_CUSTOM_CONSTRUCT
				
				CUSTOM_CONSTRUCT( Reference, ((sptr<Reference>, scopePart))((string, namePart)) )
					result->type.set_expression(result);
					result->symbol.set_reference(result);
					result->access.set_expression(result);
					result->sideEffects.set_expression(result);
				END_CUSTOM_CONSTRUCT
				
				/// The scope of this reference; a reference to a scope.
				///
				sptr<Reference> scopePart;
				
				/// The name of this reference. If omitted, this is a reference
				/// to the root, and scopePart should be null.
				///
				optional<string> namePart;
				
				/// The formal type specification of this reference. Should
				/// be function parameter types if this reference is to a
				/// function. Should be omitted otherwise. May be omitted
				/// in any case, either if automatic type deduction is to
				/// be used, or if it's a function without formal parameters.
				///
				optional<vector<sptr<Type> > > formalTypeSpec;
				
				/// The template type specification. Can be used to specify
				/// template types for functions and types. The empty list
				/// is the same as an omission in this instance. It may also
				/// be kept empty if automatic type deduction is to be used.
				///
				optional<vector<sptr<Type> > > templateTypeSpec;
				
				/// The resolved symbol of this reference. This is computed
				/// in a later phase of compilation.
				///
				class Resolved : public Computed<wptr<Symbol> > {
					void compute_value();
					wptr<Reference> _reference;
					public: void set_reference(wptr<Reference> reference);
				} symbol;
			END_CLASS
			
			////////////////////////////////////////////////////////////////////
			
			/// The literal truth-value 'true' or 'false'.
			///
			CLASS( BooleanLiteral, FROM(Expression) )
				CUSTOM_CONSTRUCT( BooleanLiteral, ((bool, value)) )
					result->type.set_expression(result);
					result->access.set_expression(result);
					result->sideEffects.set_expression(result);
				END_CUSTOM_CONSTRUCT
				
				/// The expressed truth-value.
				///
				bool value;
			END_CLASS
			
			////////////////////////////////////////////////////////////////////
			
			/// A literal integer value, bounded in size only by computer
			/// memory.
			///
			CLASS( IntegerLiteral, FROM(Expression) )
				CUSTOM_CONSTRUCT( IntegerLiteral, ((const BigInt&, value)) )
					result->type.set_expression(result);
					result->access.set_expression(result);
					result->sideEffects.set_expression(result);
				END_CUSTOM_CONSTRUCT
				
				/// The expressed integer value.
				///
				BigInt value;
			END_CLASS
			
			////////////////////////////////////////////////////////////////////
			
			/// A chain of chain-associative operators with operands. Each
			/// operand is to be evaluated once. This is used for comparison
			/// operators and implication operators.
			///
			CLASS( ChainExpression, FROM(Expression) )
				CUSTOM_CONSTRUCT( ChainExpression, )
					result->type.set_expression(result);
					result->access.set_expression(result);
					result->sideEffects.set_expression(result);
				END_CUSTOM_CONSTRUCT
				
				/// The chain-associative operators.
				///
				vector<sptr<Operator> > operators;
				
				/// The operands of this chain-operation. Should be exactly one
				/// more than the number of operators.
				///
				vector<sptr<Expression> > operands;
			END_CLASS
			
			////////////////////////////////////////////////////////////////////
				
			/// Universal Quantification expression. Returns true iff
			/// the predicate holds for all values in the range.
			///
			CLASS( ForallExpression, FROM(Expression) )
				CUSTOM_CONSTRUCT( ForallExpression, ((sptr<Identifier>, boundVar))((sptr<Expression>, lowerBound))((sptr<Expression>, upperBound))((sptr<Expression>, predicate)) )
					result->type.set_expression(result);
					result->access.set_expression(result);
					result->sideEffects.set_expression(result);
				END_CUSTOM_CONSTRUCT
				
				/// The name of the variable to be bound.
				///
				sptr<Identifier> boundVar;
				
				/// The lower bound to the variable.
				///
				sptr<Expression> lowerBound;
				
				/// The upper bound to the variable.
				///
				sptr<Expression> upperBound;
				
				/// The predicate, containing the bound variable, to be tested
				/// for all elements in the range.
				///
				sptr<Expression> predicate;
			END_CLASS
			
			////////////////////////////////////////////////////////////////////
			
			/// Existential Quantification expression. Returns true iff
			/// the predicate holds for any value in the range.
			///
			CLASS( ThereisExpression, FROM(Expression) )
				CUSTOM_CONSTRUCT( ThereisExpression, ((sptr<Identifier>, boundVar))((sptr<Expression>, lowerBound))((sptr<Expression>, upperBound))((sptr<Expression>, predicate)) )
					result->type.set_expression(result);
					result->access.set_expression(result);
					result->sideEffects.set_expression(result);
				END_CUSTOM_CONSTRUCT
				
				/// The name of the variable to be bound.
				///
				sptr<Identifier> boundVar;
				
				/// The lower bound to the variable.
				///
				sptr<Expression> lowerBound;
				
				/// The upper bound to the variable.
				///
				sptr<Expression> upperBound;
				
				/// The predicate, containing the bound variable, to be tested
				/// for all elements in the range.
				///
				sptr<Expression> predicate;
			END_CLASS

////////////////////////////////////////////////////////////////////////////////
// Function Declarations                                                      //
////////////////////////////////////////////////////////////////////////////////

/// Merge two Declarations nodes (\a a and \a b) into one.
///
sptr<Declarations> merged_declarations(wptr<Declarations> a, wptr<Declarations> b);

/// \return true , if AST \a a is structurally equal to AST \a b.
///         false, otherwise
///
bool equal(wptr<Node> a, wptr<Node> b);

/// A predicate for ordering two AST subtrees.
///
bool before(wptr<Node> a, wptr<Node> b);

/// \return  true, if \a a and type \a b are the same type.
///
bool same_type(wptr<Type> a, wptr<Type> b,
	map<wptr<Symbol>, wptr<Type> >& translations ///< lists / will list the template symbols that may appear
);

/// \return  true, if \a a and type \a b are the same type.
///
bool same_type(wptr<Type> a, wptr<Type> b);

/// \return new references to the functions of a compound/single operator
///
vector<sptr<Reference> > get_operator_references(wptr<Operator> op, vector<wptr<Expression> > operands, wptr<Symbol> scope);

/// \return a map between symbols to logical variables and their simple-form expression,
///         for those logical vars that have a simple form in the precondition
///
map<wptr<Symbol>, sptr<Node> > logical_var_simple_forms(wptr<FunctionDeclaration> decl);

/// A function object to order a list of nodes.
///
class TypeListOrder {
	public:
		bool operator()(const vector<wptr<Type> >& a, const vector<wptr<Type> >& b) const;
		bool operator()(const vector<sptr<Type> >& a, const vector<sptr<Type> >& b) const;
};

#endif // TREE_HPP
